% thom fruehwirth ECRC 1991-1993
% 910528 started boolean,and,or constraints
% 910904 added exor,neg constraints
% 911120 added imp constraint
% 931110 ported to new release
% 931111 added card constraint 

handler bool.

constraints boolean/1, and/3, or/3, exor/3, neg/2, imp/2.

%:- nodbgcomp. %!

option(check_guard_bindings, off).
option(already_in_heads, off).


boolean(0) <=> true.
boolean(1) <=> true.

label_with boolean(A) if true.
boolean(0).
boolean(1).


% and/3 specification
%and(0,0,0).
%and(0,1,0).
%and(1,0,0).
%and(1,1,1).

and(0,X,Y) <=> Y=0.
and(X,0,Y) <=> Y=0.
and(1,X,Y) <=> Y=X.
and(X,1,Y) <=> Y=X.
and(X,Y,1) <=> X=1,Y=1.
and(X,X,Z) <=> X=Z.
%and(X,Y,X) <=> imp(X,Y).
%and(X,Y,Y) <=> imp(Y,X).
and(X,Y,A) \ and(X,Y,B) <=> A=B.
and(X,Y,A) \ and(Y,X,B) <=> A=B.

label_with and(A,B,C) if true.
and(0,X,0).
and(1,X,X).
%and(X,X,X).
%and(X,Y,0):- neg(X,Y).


% or/3 specification
%or(0,0,0).
%or(0,1,1).
%or(1,0,1).
%or(1,1,1).

or(0,X,Y) <=> Y=X.
or(X,0,Y) <=> Y=X.
or(X,Y,0) <=> X=0,Y=0.
or(1,X,Y) <=> Y=1.
or(X,1,Y) <=> Y=1.
or(X,X,Z) <=> X=Z.
%or(X,Y,X) <=> imp(Y,X).
%or(X,Y,Y) <=> imp(X,Y).
or(X,Y,A) \ or(X,Y,B) <=> A=B.
or(X,Y,A) \ or(Y,X,B) <=> A=B.

label_with or(A,B,C) if true.
or(0,X,X).
or(1,X,1).
%or(X,X,X).
%or(X,Y,1):- neg(X,Y).


% exor/3 specification
%exor(0,0,0).
%exor(0,1,1).
%exor(1,0,1).
%exor(1,1,0).

exor(0,X,Y) <=> X=Y.
exor(X,0,Y) <=> X=Y.
exor(X,Y,0) <=> X=Y.
exor(1,X,Y) <=> neg(X,Y).
exor(X,1,Y) <=> neg(X,Y).
exor(X,Y,1) <=> neg(X,Y).
exor(X,X,Y) <=> Y=0.
exor(X,Y,X) <=> Y=0.
exor(Y,X,X) <=> Y=0.
exor(X,Y,A) \ exor(X,Y,B) <=> A=B.
exor(X,Y,A) \ exor(Y,X,B) <=> A=B.

label_with or(A,B,C) if true.
exor(0,X,X).
exor(1,X,Y):- neg(X,Y).
%exor(X,X,0).
%exor(X,Y,1):- neg(X,Y).


% neg/2 specification
%neg(0,1).
%neg(1,0).

neg(0,X) <=> X=1.
neg(X,0) <=> X=1.
neg(1,X) <=> X=0.
neg(X,1) <=> X=0.
neg(X,X) <=> fail.
neg_neg @ neg(X,Y) \ neg(Y,Z) <=> X=Z.	
neg_neg @ neg(X,Y) \ neg(Z,Y) <=> X=Z.	
neg_neg @ neg(Y,X) \ neg(Y,Z) <=> X=Z.	
% Interaction with other boolean constraints
neg(X,Y) \ and(X,Y,Z) <=> Z=0.
neg(Y,X) \ and(X,Y,Z) <=> Z=0.
neg(X,Z) , and(X,Y,Z) <=> X=1,Y=0,Z=0.
neg(Z,X) , and(X,Y,Z) <=> X=1,Y=0,Z=0.
neg(Y,Z) , and(X,Y,Z) <=> X=0,Y=1,Z=0.
neg(Z,Y) , and(X,Y,Z) <=> X=0,Y=1,Z=0.
neg(X,Y) \ or(X,Y,Z) <=> Z=1.
neg(Y,X) \ or(X,Y,Z) <=> Z=1.
neg(X,Z) , or(X,Y,Z) <=> X=0,Y=1,Z=1.
neg(Z,X) , or(X,Y,Z) <=> X=0,Y=1,Z=1.
neg(Y,Z) , or(X,Y,Z) <=> X=1,Y=0,Z=1.
neg(Z,Y) , or(X,Y,Z) <=> X=1,Y=0,Z=1.
neg(X,Y) \ exor(X,Y,Z) <=> Z=1.
neg(Y,X) \ exor(X,Y,Z) <=> Z=1.
neg(X,Z) \ exor(X,Y,Z) <=> Y=1.
neg(Z,X) \ exor(X,Y,Z) <=> Y=1.
neg(Y,Z) \ exor(X,Y,Z) <=> X=1.
neg(Z,Y) \ exor(X,Y,Z) <=> X=1.
neg(X,Y) , imp(X,Y) <=> X=0,Y=1.
neg(Y,X) , imp(X,Y) <=> X=0,Y=1.

label_with neg(A,B) if true.
neg(0,1).
neg(1,0).


% imp/2 specification
%imp(0,0).
%imp(0,1).
%imp(1,1).

imp(0,X) <=> true.
imp(X,0) <=> X=0.
imp(1,X) <=> X=1.
imp(X,1) <=> true.
imp(X,X) <=> true.
imp(X,Y),imp(Y,X) <=> X=Y.	

label_with imp(A,B) if true.
imp(0,X).
imp(1,1).
%imp(X,X).
%imp(0,1).



% Boolean cardinality operator
% card(A,B,L,N) constrains list L of length N to have between A and B 1s

constraints card/4.

card(A,B,L):- 
	length(L,N), 
	A=<B,0=<B,A=<N,%0=<N 		% negariant of the constraint
	card(A,B,L,N).

% card/4 specification
%card(A,B,[],0):- A=<0,0=<B.
%card(A,B,[0|L],N):-
%		N1 is N-1,
%		card(A,B,L,N1).
%card(A,B,[1|L],N):-  
%		A1 is A-1, B1 is B-1, N1 is N-1,
%		card(A1,B1,L,N1).

% Following operational specification from Pascal Van Hentenryck
triv_sat @ card(A,B,L,N) <=> A=<0,N=<B | true.		% trivial satisfaction
pos_sat @ card(N,B,L,N) <=> set_to_ones(L).		% positive satisfaction
neg_sat @ card(A,0,L,N) <=> set_to_zeros(L).		% negative satisfaction
pos_red @ card(A,B,L,N) <=> delete(X,L,L1),X==1 | 	% positive reduction
		A1 is A-1, B1 is B-1, N1 is N-1,
		card(A1,B1,L1,N1).
neg_red @ card(A,B,L,N) <=> delete(X,L,L1),X==0 | 	% negative reduction
		N1 is N-1,
		card(A,B,L1,N1).
% New special cases with two variables
card2nand @ card(0,1,[X,Y],2) <=> and(X,Y,0).		
card2neg @ card(1,1,[X,Y],2) <=> neg(X,Y).		
card2or @ card(1,2,[X,Y],2) <=> or(X,Y,1).		

label_with card(A,B,L,N) if true.
card(A,B,[],0):- A=<0,0=<B.
card(A,B,[0|L],N):-
		N1 is N-1,
		card(A,B,L).
card(A,B,[1|L],N):-  
		A1 is A-1, B1 is B-1, N1 is N-1,
		card(A1,B1,L).

  set_to_ones([]).
  set_to_ones([1|L]):-
	set_to_ones(L).

  set_to_zeros([]).
  set_to_zeros([0|L]):-
	set_to_zeros(L).



% Auxiliary predicates

operator(100,fy,(~~)).
operator(100,xfy,(#)).

  solve_bool(A,C) :- var(A), !, A=C.
  solve_bool(A,C) :- atomic(A), !, A=C.
  solve_bool(A * B, C) ?- !,
        solve_bool(A,A1),
        solve_bool(B,B1),
        and(A1,B1,C).
  solve_bool(A + B, C) ?- !,
        solve_bool(A,A1),
        solve_bool(B,B1),
        or(A1,B1,C).
  solve_bool(A # B, C) ?- !,
        solve_bool(A,A1),
        solve_bool(B,B1),
        exor(A1,B1,C).
  solve_bool(~~A,C) ?- !, 
        solve_bool(A,A1),
        neg(A1,C).
  solve_bool(A -> B, C) ?- !,
        solve_bool(A,A1),
        solve_bool(B,B1),
        imp(A1,B1),C=1.
  solve_bool(A = B, C) ?- !,
        solve_bool(A,A1),
        solve_bool(B,B1),
        A1=B1,C=1.

  bool_portray(and(A,B,C),Out)?- !, Out = (A*B = C).
  bool_portray(or(A,B,C),Out)?- !, Out = (A+B = C).
  bool_portray(exor(A,B,C),Out)?- !, Out = (A#B = C).
  bool_portray(neg(A,B),Out)?- !, Out = (A= ~~B).
  bool_portray(imp(A,B),Out)?- !, Out = (A -> B).
  bool_portray(card(A,B,L,N),Out)?- !, Out = card(A,B,L).
	
  :- define_macro(type(compound),bool_portray/2,[write]).

% Labeling 
  label_bool([]).
  label_bool([X|L]) :-
	(X=0;X=1),
	label_bool(L).

/* end of handler bool */